import java.util.*;
import org.apache.commons.lang3.ArrayUtils;;
public class SortedIntegers {
    //TODO clean
    private  /*@ spec_public @*/ int arr[];

    private /*@ spec_public @*/ int capacity, size;
    
    /*@ invariant capacity >=0; @*/
    
    /*@ invariant size >= 0; @*/
    
    /*@ invariant size <= capacity; @*/
    
    /*@ invariant arr != null; @*/
    
    // invariant for the sorted condition. 
    /*@ public invariant (\forall int a; 0 < a && a < size; arr[a-1] <= arr[a]); @*/
    //ex {1,2,3,4,7,9,10} largest number to the right of the array. 
    // you could simply say it's sorted in every state.
    
    // Why not move this to a separate junit test class ?
    public static void main (String[] args) {	
    	// Just some simple tests to see that i works  
    	SortedIntegers sort = new SortedIntegers(10);
    	System.out.println("Cap: " + sort.getCapacity());
    	sort.add(1); sort.add(2); sort.add(3); sort.add(4); sort.add(3);
    	
    	System.out.println("Added");
    	
    	for(int i = 0; i < sort.arr.length ; i++){
    		System.out.println(sort.arr[i]);
    	}
    	
    	System.out.println("Remove");
    	
    	sort.remove(2);
    	for(int i = 0; i < sort.arr.length ; i++){
    		System.out.println(sort.arr[i]);
    	}
    	
    	System.out.println("Contains: ");
    	if(sort.contains(1))
    		System.out.println("YES");
    	else
    		System.out.println("NO");
    	
    	
    	System.out.println("Max: " + sort.max());
      		
    }
    

    public SortedIntegers(int capacity) {
        this.capacity = capacity;
        this.arr = new int[capacity];
        // We fill it with initial values in order to make it work. Otherwise
        // we will be facing issues with bugs in the Array.
        Arrays.fill(arr, Integer.MAX_VALUE);
    }
    
   /*@ public normal_behavior
     @ requires capacity > size;
     @ ensures contains(elem);
     @ ensures size == \old(size)+1;
     @ ensures \forall int i; i >= 0 && i < \old(arr).length; 
     @     \old(this).contains(\old(arr)[i]) <==> this.contains(\old(arr)[i]);
     @
     @ also
     @
     @ requires capacity == size;
     @ ensures !contains(elem);
     @ ensures size == \old(size);
     @ ensures \forall int i; i >= 0 && i < \old(arr).length; 
     @     \old(this).contains(\old(arr)[i]) <==> this.contains(\old(arr)[i]);
     @*/
    
    // What I am thinking here is that we make sure that
    // if the element was in the old array than it is also in the "new" array.
    // I believe that it can be done something like this. 
    
    /*
     * (\forall Object x; this.contains(x);
	  @ arr[(Math.abs(x.hashCode())%arr.length)].contains(x));
     */
    
    
    //may include duplicates!
    // adds an element too arr which increases the size
    // We assumed that you were not able to add if the capacity was reached. 
    public void add(int elem) {
    	
    	if(++size < capacity){
    		
    	arr[size] = elem;

    	}
    	Arrays.sort(arr);
    	
    }

    // It does not matter either or not the element is in the array when we enter
    // the method, it will not be in the array afterwards anyway... 
   /*@ public normal_behavior
     @ requires contains(elem);
     @ ensures !contains(elem);
     @ ensures size < \old(size);
     @ ensures \forall int i; i >= 0 && i < \old(arr).length; 
     @     \old(this).contains(\old(arr)[i]) <==> this.contains(\old(arr)[i]);
     @
     @ also
     @ 
     @ requires !contains(elem);
     @ ensures !contains(elem);
     @ ensures size == \old(size);
     @ ensures \forall int i; i >= 0 && i < \old(arr).length; 
     @     \old(this).contains(\old(arr)[i]) <==> this.contains(\old(arr)[i]);
     @ 
     @*/
    // removes a number of elements from arr if it exists and the size is 
    // then reduced. 
    
    public void remove(int elem) {
    	
    	for(int i = 0; i <arr.length; i++){
    		if(arr[i] == elem)
    			 ArrayUtils.removeElement(arr,i);
	
    	}
    	Arrays.sort(arr);

    }

    /*@ public normal_behavior
      @ ensures \result == (\exists int a; 0<=a && a< size; arr[a] == elem);
      @*/
    
    public /*@ pure @*/ boolean contains(int elem) {
        // Search for the specified element in the array and returns true if
    	// it exists in the array.
    	//
    	for(int i = 0; i <arr.length; i++){
    		if(arr[i] == elem)
    			return true;
    	}
    		return false;
    }
    
   /*@ public normal_behavior
     @ requires size > 0;
     @ ensures \result == (\max int a; 0<=a && a<=arr.length; arr[a]);
     @ also
     @ requires size == 0;
     @ ensures \result == 0;
     @*/
    //This could be done easier by just typing: \result == arr[size-1] 

    public int max() {
    	
    	if(size>0)
    	return arr[size-1];
    	else
    		return 0;
    }
    
  /*@ public normal_behavior
    @ ensures \result == size;
    @*/
    public int getSize() {
        // return the size
    	return size;
    }
    
   /*@ public normal_behavior
     @ ensures \result == capacity;
     @*/
    public int getCapacity() {
        // return the capacity
    	return capacity;
    }
    
    /*
     * Not supposed to be commented using JML
     */
    public String toString() {
    	// Creates a string of the format: "x1, x2, x3,..., xn." 
    	String s = "";
    	for(int i = 0; i <arr.length; i++){
    		s = s+ ", " + arr[i];
    	}
    	return s+".";
    	
    	/*\\\\\\\\\\\\\ Why not simply \\\\\\\\\\\\\
    	 * return Arrays.toString(arr);
    	 * \\\\\\\\\\\\\ or \\\\\\\\\\\\\\\\\\\\\\\\
    	 * StringBuilder b = new StringBuilder(3 * arr.length).append("\"");
    	 * for (int i = 0, len = arr.length - 1; i < len; i++) {
    	 *     b.append(arr[i]).append(", ");
    	 * }
    	 * return b.append(arr[arr.length - 1]).append("\".").toString();
    	 */
    	
    }
   
}
